FDL - Nuprl Definition : interleaved

Nuprl Definition : interleaved_family

4,23

interleaved_family(T;I;L;L2)
==

f:(i:I

||L(i)||

||L2||). interleaved_family_occurence(T;I;L;L2;f)

clarification:

interleaved_family(T;I;L;L2)
==

f:(i:I

{0..||L(i)||

}

{0..||L2||

}). interleaved_family_occurence(T;I;L;L2;f)

Definitions x:A. B(x), {i..j}, ||as||, interleaved_family_occurence(T;I;L;L2;f)

FDL editor aliases interleaved_family

Definitions	x:A. B(x), {i..j}, \|\|as\|\|, interleaved_family_occurence(T;I;L;L2;f)
FDL editor aliases	interleaved_family